1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro
  5  -/
  6  
  7  import tactic.ring data.num.lemmas data.tree
src         └─────────┘ └─────────────┘ └───────┘
  8  import tactic.converter.interactive
src         └──────────────────────────┘
  9  
 10  /-!
 11  # ring2
 12  
 13  An experimental variant on the `ring` tactic that uses computational
 14  reflection instead of proof generation. Useful for kernel benchmarking.
 15  -/
 16  
 17  namespace tree
 18  
 19  /-- `(reflect' t u α)` quasiquotes a tree `(t: tree expr)` of quoted
 20  values of type `α` at level `u` into an `expr` which reifies to a `tree α`
 21  containing the reifications of the `expr`s from the original `t`. -/
 22  protected meta def reflect' (u : level) (α : expr) : tree expr → expr
id                                    └───┘       └──┘    └──┘ └──┘  └──┘
src                                   └───┘       └──┘    └──┘ └──┘   └──┘
typ                                   └───┘       └──┘    └──┘ └──┘  └──┘
doc                                   └───┘       └──┘         └──┘   └──┘
 23  | tree.nil := (expr.const ``tree.nil [u] : expr) α
id     └──────┘     └────────┘              └──┘  
src    └──────┘     └────────┘               └──┘
typ    └──────┘     └────────┘              └──┘  
doc                                             └──┘
 24  | (tree.node a t₁ t₂) :=
id      └───────┘  └┘ └┘
src     └───────┘
typ     └───────┘  └┘ └┘
 25    (expr.const ``tree.node [u] : expr) α a t₁.reflect' t₂.reflect'
id      └────────┘               └──┘  
src     └────────┘                └──┘
typ     └────────┘               └──┘  
doc                                  └──┘
 26  
 27  /-- Returns an element indexed by `n`, or zero if `n` isn't a valid index.
 28  See `tree.get`. -/
 29  protected def get_or_zero {α} [has_zero α] (t : tree α) (n : pos_num) : α :=
id                                  └──────┘        └──┘        └─────┘    
src                                 └──────┘         └──┘         └─────┘
typ                                 └──────┘        └──┘        └─────┘    
doc                                                               └─────┘
 30    t.get_or_else n 0
id     └──────────┘ 
src     └──────────┘
typ    └──────────┘ 
doc     └──────────┘
 31  
 32  end tree
 33  
 34  namespace tactic.ring2
 35  
 36  /-- A reflected/meta representation of an expression in a commutative
 37  semiring. This representation is a direct translation of such
 38  expressions - see `horner_expr` for a normal form. -/
 39  @[derive has_reflect]
id            └─────────┘
src           └─────────┘
typ           └─────────┘
doc    └────┘
 40  inductive csring_expr
 41  /- (atom n) is an opaque element of the csring. For example,
 42  a local variable in the context. n indexes into a storage
 43  of such atoms - a `tree α`. -/
 44  | atom : pos_num → csring_expr
id            └─────┘
src           └─────┘
typ           └─────┘
doc           └─────┘
 45  /- (const n) is technically the csring's one, added n times.
 46  Or the zero if n is 0. -/
 47  | const : num → csring_expr
id             └─┘
src            └─┘
typ            └─┘
doc            └─┘
 48  | add : csring_expr → csring_expr → csring_expr
 49  | mul : csring_expr → csring_expr → csring_expr
 50  | pow : csring_expr → num → csring_expr
id                         └─┘
src                        └─┘
typ                        └─┘
doc                        └─┘
 51  
 52  namespace csring_expr
 53  
 54  instance : inhabited csring_expr := ⟨const 0⟩
id              └───────┘ └─────────┘     └───┘
src             └───────┘ └─────────┘     └───┘
typ             └───────┘ └─────────┘     └───┘
doc                       └─────────┘
 55  
 56  /-- Evaluates a reflected `csring_expr` into an element of the
 57  original `comm_semiring` type `α`, retrieving opaque elements
 58  (atoms) from the tree `t`. -/
 59  def eval {α} [comm_semiring α] (t : tree α) : csring_expr → α
id                 └───────────┘        └──┘     └─────────┘  
src                └───────────┘         └──┘      └─────────┘
typ                └───────────┘        └──┘     └─────────┘  
doc                                                └─────────┘
 60  | (atom n)  := t.get_or_zero n
id      └──┘       └──────────┘
src     └──┘         └──────────┘
typ     └──┘       └──────────┘
doc                  └──────────┘
 61  | (const n) := n
id      └───┘ 
src     └───┘
typ     └───┘ 
 62  | (add x y) := eval x + eval y
id      └─┘       └──┘    └──┘
src     └─┘                
typ     └─┘       └──┘    └──┘
 63  | (mul x y) := eval x * eval y
id      └─┘       └──┘    └──┘
src     └─┘                
typ     └─┘       └──┘    └──┘
 64  | (pow x n) := eval x ^ (n : ℕ)
id      └─┘       └──┘         
src     └─┘                      
typ     └─┘       └──┘         
 65  
 66  end csring_expr
 67  
 68  /-- An efficient representation of expressions in a commutative
 69  semiring using the sparse Horner normal form. This type admits
 70  non-optimal instantiations (e.g. `P` can be represented as `P+0+0`),
 71  so to get good performance out of it, care must be taken to maintain
 72  an optimal, *canonical* form. -/
 73  @[derive decidable_eq]
id            └──────────┘
src           └──────────┘
typ           └──────────┘
doc    └────┘
 74  inductive horner_expr
 75  /- (const n) is a constant n in the csring, similarly to the same
 76  constructor in `csring_expr`. This one, however, can be negative. -/
 77  | const : znum → horner_expr
id             └──┘
src            └──┘
typ            └──┘
doc            └──┘
 78  /- (horner a x n b) is a*xⁿ + b, where x is the x-th atom
 79  in the atom tree. -/
 80  | horner : horner_expr → pos_num → num → horner_expr → horner_expr
id                            └─────┘   └─┘
src                           └─────┘   └─┘
typ                           └─────┘   └─┘
doc                           └─────┘   └─┘
 81  
 82  namespace horner_expr
 83  
 84  /-- True iff the `horner_expr` argument is a valid `csring_expr`.
 85  For that to be the case, all its constants must be non-negative. -/
 86  def is_cs : horner_expr → Prop
id               └─────────┘ 
src              └─────────┘
typ              └─────────┘ 
doc              └─────────┘
 87  | (const n) := ∃ m:num, n = m.to_znum
id      └───┘         └─┘    └──────┘
src     └───┘          └─┘     └──────┘
typ     └───┘         └─┘    └──────┘
doc                     └─┘
 88  | (horner a x n b) := is_cs a ∧ is_cs b
id      └────┘           └───┘    └───┘
src     └────┘                     
typ     └────┘           └───┘    └───┘
 89  
 90  instance : has_zero horner_expr := ⟨const 0⟩
id              └──────┘ └─────────┘     └───┘
src             └──────┘ └─────────┘     └───┘
typ             └──────┘ └─────────┘     └───┘
doc                      └─────────┘
 91  instance : has_one horner_expr := ⟨const 1⟩
id              └─────┘ └─────────┘     └───┘
src             └─────┘ └─────────┘     └───┘
typ             └─────┘ └─────────┘     └───┘
doc                     └─────────┘
 92  instance : inhabited horner_expr := ⟨0⟩
id              └───────┘ └─────────┘
src             └───────┘ └─────────┘
typ             └───────┘ └─────────┘
doc                       └─────────┘
 93  
 94  /-- Represent a `csring_expr.atom` in Horner form. -/
 95  def atom (n : pos_num) : horner_expr := horner 1 n 1 0
id                 └─────┘    └─────────┘    └────┘   
src                └─────┘    └─────────┘    └────┘
typ                └─────┘    └─────────┘    └────┘   
doc                └─────┘    └─────────┘
 96  
 97  def to_string : horner_expr → string
id                   └─────────┘  └────┘
src                  └─────────┘  └────┘
typ                  └─────────┘  └────┘
doc                  └─────────┘
 98  | (const n) := _root_.repr n
id      └───┘      └─────────┘
src     └───┘       └─────────┘
typ     └───┘      └─────────┘
 99  | (horner a x n b) :=
id      └────┘    
src     └────┘
typ     └────┘    
100      "(" ++ to_string a ++ ") * x" ++ _root_.repr x ++ "^"
id           └┘ └───────┘   └┘         └┘ └─────────┘   └┘
src          └┘ └───────┘   └┘         └┘ └─────────┘   └┘
typ          └┘ └───────┘   └┘         └┘ └─────────┘   └┘
101          ++ _root_.repr n ++ " + " ++ to_string b
id           └┘ └─────────┘   └┘       └┘ └───────┘
src          └┘ └─────────┘   └┘       └┘ └───────┘
typ          └┘ └─────────┘   └┘       └┘ └───────┘
102  instance : has_to_string horner_expr := ⟨to_string⟩
id              └───────────┘ └─────────┘     └───────┘
src             └───────────┘ └─────────┘     └───────┘
typ             └───────────┘ └─────────┘     └───────┘
doc                           └─────────┘
103  
104  /-- Alternative constructor for (horner a x n b) which maintains canonical
105  form by simplifying special cases of `a`. -/
106  def horner' (a : horner_expr)
id                    └─────────┘
src                   └─────────┘
typ                   └─────────┘
doc                   └─────────┘
107    (x : pos_num) (n : num) (b : horner_expr) : horner_expr :=
id          └─────┘       └─┘       └─────────┘    └─────────┘
src         └─────┘       └─┘       └─────────┘    └─────────┘
typ         └─────┘       └─┘       └─────────┘    └─────────┘
doc         └─────┘       └─┘       └─────────┘    └─────────┘
108  match a with
id         
typ        
109  | const q := if q = 0 then b else horner a x n b
id     └───┘                        └────┘    
src    └───┘                          └────┘
typ    └───┘                        └────┘    
110  | horner a₁ x₁ n₁ b₁ :=
id     └────┘ └┘ └┘ └┘ └┘
src    └────┘
typ    └────┘ └┘ └┘ └┘ └┘
111    if x₁ = x ∧ b₁ = 0 then horner a₁ x (n₁ + n) b
id                         └────┘            
src                         └────┘          
typ                        └────┘            
112    else horner a x n b
id          └────┘    
src         └────┘
typ         └────┘    
113  end
114  
115  def add_const (k : znum) (e : horner_expr) : horner_expr :=
id                      └──┘       └─────────┘    └─────────┘
src                     └──┘       └─────────┘    └─────────┘
typ                     └──┘       └─────────┘    └─────────┘
doc                     └──┘       └─────────┘    └─────────┘
116  if k = 0 then e else begin
id               
src       
typ              
st                        └─────
117    induction e with n a x n b A B,
id               
src    └────────┘ └─────────────────┘
typ    └────────┘└─────────────────┘
doc    └────────┘ └─────────────────┘
txt    └────────┘ └─────────────────┘
par    └────────┘ └─────────────────┘
pid              └────────────────┘
st   ───────────────────────────────┘└─
118    { exact const (k + n) },
id             └───┘    
src      └────┘└───┘   └┘
typ      └────┘└───┘ └┘
doc      └────┘         └┘
txt      └────┘         └┘
par      └────┘         └┘
pid                    
st   ───┘└──────────────────┘└┘
119    { exact horner a x n B }
id             └────┘    
src      └────┘└────┘    
typ      └────┘└────┘
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ────────────────────────┘└─
120  end
st   ──┘
121  
122  def add_aux (a₁ : horner_expr) (A₁ : horner_expr → horner_expr) (x₁ : pos_num) :
id                     └─────────┘        └─────────┘   └─────────┘        └─────┘
src                    └─────────┘        └─────────┘   └─────────┘        └─────┘
typ                    └─────────┘        └─────────┘   └─────────┘        └─────┘
doc                    └─────────┘        └─────────┘   └─────────┘        └─────┘
123    horner_expr → num → horner_expr → (horner_expr → horner_expr) → horner_expr
id     └─────────┘  └─┘   └─────────┘    └─────────┘  └─────────┘    └─────────┘
src    └─────────┘   └─┘   └─────────┘    └─────────┘   └─────────┘    └─────────┘
typ    └─────────┘  └─┘   └─────────┘    └─────────┘  └─────────┘    └─────────┘
doc    └─────────┘   └─┘   └─────────┘    └─────────┘   └─────────┘    └─────────┘
124  | (const n₂)           n₁ b₁ B₁ := add_const n₂ (horner a₁ x₁ n₁ b₁)
id      └───┘ └┘            └┘ └┘       └───────┘     └────┘ └┘ └┘
src     └───┘                           └───────┘     └────┘
typ     └───┘ └┘            └┘ └┘       └───────┘     └────┘ └┘ └┘
125  | (horner a₂ x₂ n₂ b₂) n₁ b₁ B₁ :=
id      └────┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘
src     └────┘
typ     └────┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘
126    let e₂ := horner a₂ x₂ n₂ b₂ in
id         └┘    └────┘
src              └────┘
typ        └┘    └────┘
127    match pos_num.cmp x₁ x₂ with
id           └─────────┘ └┘
src          └─────────┘
typ          └─────────┘ └┘
128    | ordering.lt := horner a₁ x₁ n₁ (B₁ e₂)
id       └─────────┘    └────┘ └┘ └┘        └┘
src      └─────────┘    └────┘
typ      └─────────┘    └────┘ └┘ └┘        └┘
129    | ordering.gt := horner a₂ x₂ n₂ (add_aux b₂ n₁ b₁ B₁)
id       └─────────┘    └────┘           └─────┘
src      └─────────┘    └────┘
typ      └─────────┘    └────┘           └─────┘
130    | ordering.eq :=
id       └─────────┘
src      └─────────┘
typ      └─────────┘
131      match num.sub' n₁ n₂ with
id             └──────┘
src            └──────┘
typ            └──────┘
132      | znum.zero := horner' (A₁ a₂) x₁ n₁ (B₁ b₂)
id         └───────┘    └─────┘  └┘     └┘
src        └───────┘    └─────┘
typ        └───────┘    └─────┘  └┘     └┘
doc                     └─────┘
133      | (znum.pos k) := horner (add_aux a₂ k 0 id) x₁ n₂ (B₁ b₂)
id          └──────┘      └────┘  └─────┘        └┘  └┘
src         └──────┘       └────┘                 └┘
typ         └──────┘      └────┘  └─────┘        └┘  └┘
134      | (znum.neg k) := horner (A₁ (horner a₂ x₁ k 0)) x₁ n₁ (B₁ b₂)
id          └──────┘      └────┘  └┘  └────┘    └┘       └┘
src         └──────┘       └────┘      └────┘
typ         └──────┘      └────┘  └┘  └────┘    └┘       └┘
135      end
136    end
137  
138  def add : horner_expr → horner_expr → horner_expr
id             └─────────┘  └─────────┘   └─────────┘
src            └─────────┘   └─────────┘   └─────────┘
typ            └─────────┘  └─────────┘   └─────────┘
doc            └─────────┘   └─────────┘   └─────────┘
139  | (const n₁)           e₂ := add_const n₁ e₂
id      └───┘ └┘            └┘    └───────┘
src     └───┘                     └───────┘
typ     └───┘ └┘            └┘    └───────┘
140  | (horner a₁ x₁ n₁ b₁) e₂ := add_aux a₁ (add a₁) x₁ e₂ n₁ b₁ (add b₁)
id      └────┘ └┘ └┘ └┘ └┘  └┘    └─────┘     └─┘                  └─┘
src     └────┘                    └─────┘
typ     └────┘ └┘ └┘ └┘ └┘  └┘    └─────┘     └─┘                  └─┘
141  /-begin
142    induction e₁ with n₁ a₁ x₁ n₁ b₁ A₁ B₁ generalizing e₂,
143    { exact add_const n₁ e₂ },
144    exact match e₂ with e₂ := begin
145      induction e₂ with n₂ a₂ x₂ n₂ b₂ A₂ B₂ generalizing n₁ b₁;
146      let e₁ := horner a₁ x₁ n₁ b₁,
147      { exact add_const n₂ e₁ },
148      let e₂ := horner a₂ x₂ n₂ b₂,
149      exact match pos_num.cmp x₁ x₂ with
150      | ordering.lt := horner a₁ x₁ n₁ (B₁ e₂)
151      | ordering.gt := horner a₂ x₂ n₂ (B₂ n₁ b₁)
152      | ordering.eq :=
153        match num.sub' n₁ n₂ with
154        | znum.zero := horner' (A₁ a₂) x₁ n₁ (B₁ b₂)
155        | (znum.pos k) := horner (A₂ k 0) x₁ n₂ (B₁ b₂)
156        | (znum.neg k) := horner (A₁ (horner a₂ x₁ k 0)) x₁ n₁ (B₁ b₂)
157        end
158      end
159    end end
160  end-/
161  
162  def neg (e : horner_expr) : horner_expr :=
id                └─────────┘    └─────────┘
src               └─────────┘    └─────────┘
typ               └─────────┘    └─────────┘
doc               └─────────┘    └─────────┘
163  begin
st   └─────
164    induction e with n a x n b A B,
id               
src    └────────┘ └─────────────────┘
typ    └────────┘└─────────────────┘
doc    └────────┘ └─────────────────┘
txt    └────────┘ └─────────────────┘
par    └────────┘ └─────────────────┘
pid              └────────────────┘
st   ───────────────────────────────┘└─
165    { exact const (-n) },
id             └───┘  
src      └────┘└───┘  └┘
typ      └────┘└───┘ └┘
doc      └────┘        └┘
txt      └────┘        └┘
par      └────┘        └┘
pid                   
st   ───┘└───────────────┘└┘
166    { exact horner A x n B }
id             └────┘    
src      └────┘└────┘    
typ      └────┘└────┘
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ────────────────────────┘└─
167  end
st   ──┘
168  
169  def mul_const (k : znum) (e : horner_expr) : horner_expr :=
id                      └──┘       └─────────┘    └─────────┘
src                     └──┘       └─────────┘    └─────────┘
typ                     └──┘       └─────────┘    └─────────┘
doc                     └──┘       └─────────┘    └─────────┘
170  if k = 0 then 0 else if k = 1 then e else begin
id                                  
src                           
typ                                 
st                                             └─────
171    induction e with n a x n b A B,
id               
src    └────────┘ └─────────────────┘
typ    └────────┘└─────────────────┘
doc    └────────┘ └─────────────────┘
txt    └────────┘ └─────────────────┘
par    └────────┘ └─────────────────┘
pid              └────────────────┘
st   ───────────────────────────────┘└─
172    { exact const (n * k) },
id             └───┘    
src      └────┘└───┘   └┘
typ      └────┘└───┘ └┘
doc      └────┘         └┘
txt      └────┘         └┘
par      └────┘         └┘
pid                    
st   ───┘└──────────────────┘└┘
173    { exact horner A x n B }
id             └────┘    
src      └────┘└────┘    
typ      └────┘└────┘
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ────────────────────────┘└─
174  end
st   ──┘
175  
176  def mul_aux (a₁ x₁ n₁ b₁) (A₁ B₁ : horner_expr → horner_expr) :
id                                      └─────────┘   └─────────┘
src                                     └─────────┘   └─────────┘
typ                                     └─────────┘   └─────────┘
doc                                     └─────────┘   └─────────┘
177    horner_expr → horner_expr
id     └─────────┘  └─────────┘
src    └─────────┘   └─────────┘
typ    └─────────┘  └─────────┘
doc    └─────────┘   └─────────┘
178  | (const n₂) := mul_const n₂ (horner a₁ x₁ n₁ b₁)
id      └───┘ └┘     └───────┘     └────┘ └┘ └┘ └┘ └┘
src     └───┘        └───────┘     └────┘
typ     └───┘ └┘     └───────┘     └────┘ └┘ └┘ └┘ └┘
179  | e₂@(horner a₂ x₂ n₂ b₂) :=
id         └────┘ └┘ └┘ └┘ └┘
src        └────┘
typ        └────┘ └┘ └┘ └┘ └┘
180    match pos_num.cmp x₁ x₂ with
id           └─────────┘ └┘
src          └─────────┘
typ          └─────────┘ └┘
181    | ordering.lt := horner (A₁ e₂) x₁ n₁ (B₁ e₂)
id       └─────────┘    └────┘  └┘     └┘ └┘  └┘
src      └─────────┘    └────┘
typ      └─────────┘    └────┘  └┘     └┘ └┘  └┘
182    | ordering.gt := horner (mul_aux a₂) x₂ n₂ (mul_aux b₂)
id       └─────────┘    └────┘  └─────┘            └─────┘
src      └─────────┘    └────┘
typ      └─────────┘    └────┘  └─────┘            └─────┘
183    | ordering.eq := let haa := horner' (mul_aux a₂) x₁ n₂ 0 in
id       └─────────┘        └─┘    └─────┘  └─────┘     └┘
src      └─────────┘               └─────┘
typ      └─────────┘        └─┘    └─────┘  └─────┘     └┘
doc                                └─────┘
184      if b₂ = 0 then haa else haa.add (horner (A₁ b₂) x₁ n₁ (B₁ b₂))
id                     └─┘      └─┘└──┘  └────┘  └┘     └┘ └┘  └┘
src                                └──┘  └────┘
typ                    └─┘      └─┘└──┘  └────┘  └┘     └┘ └┘  └┘
185    end
186  
187  def mul : horner_expr → horner_expr → horner_expr
id             └─────────┘  └─────────┘   └─────────┘
src            └─────────┘   └─────────┘   └─────────┘
typ            └─────────┘  └─────────┘   └─────────┘
doc            └─────────┘   └─────────┘   └─────────┘
188  | (const n₁)           := mul_const n₁
id      └───┘ └┘               └───────┘
src     └───┘                  └───────┘
typ     └───┘ └┘               └───────┘
189  | (horner a₁ x₁ n₁ b₁) := mul_aux a₁ x₁ n₁ b₁ (mul a₁) (mul b₁).
id      └────┘ └┘ └┘ └┘ └┘     └─────┘              └─┘      └─┘
src     └────┘                 └─────┘
typ     └────┘ └┘ └┘ └┘ └┘     └─────┘              └─┘      └─┘
190  /-begin
191    induction e₁ with n₁ a₁ x₁ n₁ b₁ A₁ B₁ generalizing e₂,
192    { exact mul_const n₁ e₂ },
193    induction e₂ with n₂ a₂ x₂ n₂ b₂ A₂ B₂;
194    let e₁ := horner a₁ x₁ n₁ b₁,
195    { exact mul_const n₂ e₁ },
196    let e₂ := horner a₂ x₂ n₂ b₂,
197    cases pos_num.cmp x₁ x₂,
198    { exact horner (A₁ e₂) x₁ n₁ (B₁ e₂) },
199    { let haa := horner' A₂ x₁ n₂ 0,
200      exact if b₂ = 0 then haa else
201        haa.add (horner (A₁ b₂) x₁ n₁ (B₁ b₂)) },
202    { exact horner A₂ x₂ n₂ B₂ }
203  end-/
204  
205  instance : has_add horner_expr := ⟨add⟩
id              └─────┘ └─────────┘     └─┘
src             └─────┘ └─────────┘     └─┘
typ             └─────┘ └─────────┘     └─┘
doc                     └─────────┘
206  instance : has_neg horner_expr := ⟨neg⟩
id              └─────┘ └─────────┘     └─┘
src             └─────┘ └─────────┘     └─┘
typ             └─────┘ └─────────┘     └─┘
doc                     └─────────┘
207  instance : has_mul horner_expr := ⟨mul⟩
id              └─────┘ └─────────┘     └─┘
src             └─────┘ └─────────┘     └─┘
typ             └─────┘ └─────────┘     └─┘
doc                     └─────────┘
208  
209  def pow (e : horner_expr) : num → horner_expr
id                └─────────┘    └─┘  └─────────┘
src               └─────────┘    └─┘   └─────────┘
typ               └─────────┘    └─┘  └─────────┘
doc               └─────────┘    └─┘   └─────────┘
210  | 0 := 1
211  | (num.pos p) := begin
id      └─────┘
src     └─────┘
typ     └─────┘
st                    └─────
212    induction p with p ep p ep,
id               
src    └────────┘ └─────────────┘
typ    └────────┘└─────────────┘
doc    └────────┘ └─────────────┘
txt    └────────┘ └─────────────┘
par    └────────┘ └─────────────┘
pid              └────────────┘
st   ───────────────────────────┘└─
213    { exact e },
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───┘└──────┘└┘
214    { exact (ep.mul ep).mul e },
id              └────┘ └┘      
src      └────┘ └────┘  └────┘ 
typ      └────┘ └────┘└┘└────┘
doc      └────┘         └────┘ 
txt      └────┘         └────┘ 
par      └────┘         └────┘ 
pid                    └────┘ 
st   ───┘└──────────────────────┘└┘
215    { exact ep.mul ep }
id             └────┘ └┘
src      └────┘└────┘  
typ      └────┘└────┘└┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ───────────────────┘└─
216  end
st   ──┘
217  
218  def inv (e : horner_expr) : horner_expr := 0
id                └─────────┘    └─────────┘
src               └─────────┘    └─────────┘
typ               └─────────┘    └─────────┘
doc               └─────────┘    └─────────┘
219  
220  /-- Brings expressions into Horner normal form. -/
221  def of_csexpr : csring_expr → horner_expr
id                   └─────────┘  └─────────┘
src                  └─────────┘   └─────────┘
typ                  └─────────┘  └─────────┘
doc                  └─────────┘   └─────────┘
222  | (csring_expr.atom n)  := atom n
id      └──────────────┘       └──┘
src     └──────────────┘        └──┘
typ     └──────────────┘       └──┘
doc                             └──┘
223  | (csring_expr.const n) := const n.to_znum
id      └───────────────┘      └───┘  └──────┘
src     └───────────────┘       └───┘  └──────┘
typ     └───────────────┘      └───┘  └──────┘
224  | (csring_expr.add x y) := (of_csexpr x).add (of_csexpr y)
id      └─────────────┘        └───────┘   └─┘   └───────┘
src     └─────────────┘                      └─┘
typ     └─────────────┘        └───────┘   └─┘   └───────┘
225  | (csring_expr.mul x y) := (of_csexpr x).mul (of_csexpr y)
id      └─────────────┘        └───────┘   └─┘   └───────┘
src     └─────────────┘                      └─┘
typ     └─────────────┘        └───────┘   └─┘   └───────┘
226  | (csring_expr.pow x n) := (of_csexpr x).pow n
id      └─────────────┘        └───────┘   └─┘
src     └─────────────┘                      └─┘
typ     └─────────────┘        └───────┘   └─┘
227  
228  /-- Evaluates a reflected `horner_expr` - see `csring_expr.eval`. -/
229  def cseval {α} [comm_semiring α] (t : tree α) : horner_expr → α
id                   └───────────┘        └──┘     └─────────┘  
src                  └───────────┘         └──┘      └─────────┘
typ                  └───────────┘        └──┘     └─────────┘  
doc                                                  └─────────┘
230  | (const n)        := n.abs
id      └───┘              └──┘
src     └───┘               └──┘
typ     └───┘              └──┘
231  | (horner a x n b) := tactic.ring.horner (cseval a) (t.get_or_zero x) n (cseval b)
id      └────┘         └────────────────┘  └────┘     └──────────┘       └────┘
src     └────┘             └────────────────┘              └──────────┘
typ     └────┘         └────────────────┘  └────┘     └──────────┘       └────┘
doc                                                        └──────────┘
232  
233  theorem cseval_atom {α} [comm_semiring α] (t : tree α)
id                            └───────────┘        └──┘ 
src                           └───────────┘         └──┘
typ                           └───────────┘        └──┘ 
234    (n : pos_num) : (atom n).is_cs ∧ cseval t (atom n) = t.get_or_zero n :=
id          └─────┘     └──┘  └───┘   └────┘   └──┘    └──────────┘ 
src         └─────┘     └──┘   └───┘   └────┘    └──┘      └──────────┘
typ         └─────┘     └──┘  └───┘   └────┘   └──┘    └──────────┘ 
doc         └─────┘     └──┘   └───┘    └────┘    └──┘       └──────────┘
235  ⟨⟨⟨1, rfl⟩, ⟨0, rfl⟩⟩, (tactic.ring.horner_atom _).symm⟩
id         └─┘       └─┘     └─────────────────────┘   └──┘
src        └─┘       └─┘     └─────────────────────┘   └──┘
typ        └─┘       └─┘     └─────────────────────┘   └──┘
236  
237  theorem cseval_add_const {α} [comm_semiring α] (t : tree α)
id                                 └───────────┘        └──┘ 
src                                └───────────┘         └──┘
typ                                └───────────┘        └──┘ 
238    (k : num) {e : horner_expr} (cs : e.is_cs) :
id          └─┘       └─────────┘        └────┘
src         └─┘       └─────────┘         └────┘
typ         └─┘       └─────────┘        └────┘
doc         └─┘       └─────────┘         └────┘
239    (add_const k.to_znum e).is_cs ∧
id      └───────┘ └──────┘  └───┘  
src     └───────┘  └──────┘   └───┘  
typ     └───────┘ └──────┘  └───┘  
doc                           └───┘
240      cseval t (add_const k.to_znum e) = k + cseval t e :=
id       └────┘   └───────┘ └──────┘      └────┘  
src      └────┘    └───────┘  └──────┘        └────┘
typ      └────┘   └───────┘ └──────┘      └────┘  
doc      └────┘                                 └────┘
241  begin
st   └─────
242    simp [add_const],
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                 
st   ─────────────────┘└─
243    cases k; simp! *,
id           
src    └────┘   └─────┘
typ    └────┘  └─────┘
doc    └────┘   └─────┘
txt    └────┘   └─────┘
par    └────┘   └─────┘
pid                
st   ─────────────────┘└─
244    simp [show znum.pos k ≠ 0, from dec_trivial],
id                └──────┘           └─────────┘
src    └────┘    └──────┘ └───────┘└─────────┘
typ    └────┘    └──────┘└───────┘└─────────┘
doc    └────┘              └───────┘└─────────┘
txt    └────┘              └───────┘           
par    └────┘              └───────┘           
pid                      └───────┘           
st   ─────────────────────────────────────────────┘└─
245    induction e with n a x n b A B; simp *,
id               
src    └────────┘ └─────────────────┘  └────┘
typ    └────────┘└─────────────────┘  └────┘
doc    └────────┘ └─────────────────┘  └────┘
txt    └────────┘ └─────────────────┘  └────┘
par    └────────┘ └─────────────────┘  └────┘
pid              └────────────────┘      
st   ───────────────────────────────────────┘└─
246    { rcases cs with ⟨n, rfl⟩,
id              └┘
src      └─────┘  └────────────┘
typ      └─────┘└┘└────────────┘
doc      └─────┘  └────────────┘
txt      └─────┘  └────────────┘
par      └─────┘  └────────────┘
pid              └────────────┘
st   ───┘└─────────────────────┘└─
247      refine ⟨⟨n + num.pos k, by simp; refl⟩, _⟩,
id                  └─────┘ 
src      └─────┘   └─────┘ └┘  └──┘└┘└──┘└───┘
typ      └─────┘  └─────┘└┘  └──┘└┘└──┘└───┘
doc      └─────┘            └┘  └──┘└┘└──┘└───┘
txt      └─────┘            └┘  └──┘└┘└──┘└───┘
par      └─────┘            └┘  └──┘└┘└──┘└───┘
pid                        └┘  └──────────────┘
st   ─────────────────────────────┘└─────────┘└───┘└─
248      cases n; simp! },
id             
src      └────┘   └────┘
typ      └────┘  └────┘
doc      └────┘   └────┘
txt      └────┘   └────┘
par      └────┘   └────┘
pid                  
st   ──────────────────┘└┘
249    { rcases B cs.2 with ⟨csb, h⟩, simp! [*, cs.1],
id               └┘                            └┘
src      └─────┘   └──────────────┘  └────────┘  └─┘
typ      └─────┘└┘└──────────────┘  └────────┘└┘└─┘
doc      └─────┘   └──────────────┘  └────────┘  └─┘
txt      └─────┘   └──────────────┘  └────────┘  └─┘
par      └─────┘   └──────────────┘  └────────┘  └─┘
pid               └──────────────┘      └──┘  └─┘
st   ──────────────────────────────┘└───────────────┘└─
250      rw [← tactic.ring.horner_add_const, add_comm], refl }
id             └──────────────────────────┘  └──────┘
src      └────┘└──────────────────────────┘└┘└──────┘  └───┘
typ      └────┘└──────────────────────────┘└┘└──────┘  └───┘
doc      └────┘                            └┘          └───┘
txt      └────┘                            └┘          └───┘
par      └────┘                            └┘          └───┘
pid        └──┘                            └┘              
st   ─────────────────────────────────────┘└────────┘└─────┘└─
251  end
st   ──┘
252  
253  theorem cseval_horner' {α} [comm_semiring α] (t : tree α)
id                               └───────────┘        └──┘ 
src                              └───────────┘         └──┘
typ                              └───────────┘        └──┘ 
254    (a x n b) (h₁ : is_cs a) (h₂ : is_cs b) :
id                     └───┘         └───┘ 
src                    └───┘          └───┘
typ                    └───┘         └───┘ 
doc                    └───┘          └───┘
255    (horner' a x n b).is_cs ∧ cseval t (horner' a x n b) =
id      └─────┘     └───┘   └────┘   └─────┘      
src     └─────┘         └───┘   └────┘    └─────┘          
typ     └─────┘     └───┘   └────┘   └─────┘      
doc     └─────┘         └───┘    └────┘    └─────┘
256      tactic.ring.horner (cseval t a) (t.get_or_zero x) n (cseval t b) :=
id       └────────────────┘  └────┘     └──────────┘     └────┘  
src      └────────────────┘  └────┘        └──────────┘       └────┘
typ      └────────────────┘  └────┘     └──────────┘     └────┘  
doc                          └────┘        └──────────┘       └────┘
257  begin
st   └─────
258    cases a with n₁ a₁ x₁ n₁ b₁; simp [horner']; split_ifs,
id                                       └─────┘
src    └────┘ └──────────────────┘  └────┘└─────┘  └───────┘
typ    └────┘└──────────────────┘  └────┘└─────┘  └───────┘
doc    └────┘ └──────────────────┘  └────┘└─────┘  └───────┘
txt    └────┘ └──────────────────┘  └────┘         └───────┘
par    └────┘ └──────────────────┘  └────┘         └───────┘
pid          └──────────────────┘             
st   ───────────────────────────────────────────────────────┘└─
259    { simp! [*, tactic.ring.horner] },
id                 └────────────────┘
src      └────────┘└────────────────┘└┘
typ      └────────┘└────────────────┘└┘
doc      └────────┘                  └┘
txt      └────────┘                  └┘
par      └────────┘                  └┘
pid          └──┘                  
st   ───┘└────────────────────────────┘└┘
260    { exact ⟨⟨h₁, h₂⟩, rfl⟩ },
id               └┘  └┘   └─┘
src      └────┘    └┘  └─┘└─┘└┘
typ      └────┘  └┘└┘└┘└─┘└─┘└┘
doc      └────┘    └┘  └─┘   └┘
txt      └────┘    └┘  └─┘   └┘
par      └────┘    └┘  └─┘   └┘
pid               └┘  └─┘   
st   ───┘└────────────────────┘└┘
261    { refine ⟨⟨h₁.1, h₂⟩, eq.symm _⟩, simp! *,
id                └┘    └┘   └─────┘
src      └─────┘    └──┘  └─┘└─────┘└─┘  └─────┘
typ      └─────┘  └┘└──┘└┘└─┘└─────┘└─┘  └─────┘
doc      └─────┘    └──┘  └─┘       └─┘  └─────┘
txt      └─────┘    └──┘  └─┘       └─┘  └─────┘
par      └─────┘    └──┘  └─┘       └─┘  └─────┘
pid                └──┘  └─┘       └─┘      
st   ───┘└────────────────────────────┘└───────┘└─
262      apply tactic.ring.horner_horner, simp },
id             └───────────────────────┘
src      └────┘└───────────────────────┘  └───┘
typ      └────┘└───────────────────────┘  └───┘
doc      └────┘                           └───┘
txt      └────┘                           └───┘
par      └────┘                           └───┘
pid                                          
st   ──────────────────────────────────┘└─────┘└┘
263    { exact ⟨⟨h₁, h₂⟩, rfl⟩ }
id               └┘  └┘   └─┘
src      └────┘    └┘  └─┘└─┘└┘
typ      └────┘  └┘└┘└┘└─┘└─┘└┘
doc      └────┘    └┘  └─┘   └┘
txt      └────┘    └┘  └─┘   └┘
par      └────┘    └┘  └─┘   └┘
pid               └┘  └─┘   
st   ─────────────────────────┘└─
264  end
st   ──┘
265  
266  theorem cseval_add {α} [comm_semiring α] (t : tree α)
id                           └───────────┘        └──┘ 
src                          └───────────┘         └──┘
typ                          └───────────┘        └──┘ 
267    {e₁ e₂ : horner_expr} (cs₁ : e₁.is_cs) (cs₂ : e₂.is_cs) :
id              └─────────┘         └┘└────┘         └┘└────┘
src             └─────────┘           └────┘           └────┘
typ             └─────────┘         └┘└────┘         └┘└────┘
doc             └─────────┘           └────┘           └────┘
268    (add e₁ e₂).is_cs ∧
id      └─┘ └┘ └┘ └───┘  
src     └─┘       └───┘  
typ     └─┘ └┘ └┘ └───┘  
doc               └───┘
269    cseval t (add e₁ e₂) = cseval t e₁ + cseval t e₂ :=
id     └────┘   └─┘ └┘ └┘   └────┘  └┘  └────┘  └┘
src    └────┘    └─┘         └────┘       └────┘
typ    └────┘   └─┘ └┘ └┘   └────┘  └┘  └────┘  └┘
doc    └────┘                 └────┘        └────┘
270  begin
st   └─────
271    induction e₁ with n₁ a₁ x₁ n₁ b₁ A₁ B₁ generalizing e₂; simp!,
id               └┘
src    └────────┘  └────────────────────────────────────────┘  └───┘
typ    └────────┘└┘└────────────────────────────────────────┘  └───┘
doc    └────────┘  └────────────────────────────────────────┘  └───┘
txt    └────────┘  └────────────────────────────────────────┘  └───┘
par    └────────┘  └────────────────────────────────────────┘  └───┘
pid               └───────────────────────┘└──────────────┘      
st   ──────────────────────────────────────────────────────────────┘└─
272    { rcases cs₁ with ⟨n₁, rfl⟩,
id              └─┘
src      └─────┘   └─────────────┘
typ      └─────┘└─┘└─────────────┘
doc      └─────┘   └─────────────┘
txt      └─────┘   └─────────────┘
par      └─────┘   └─────────────┘
pid               └─────────────┘
st   ───┘└───────────────────────┘└─
273      simpa using cseval_add_const t n₁ cs₂ },
id                   └──────────────┘  └┘ └─┘
src      └──────────┘└──────────────┘      
typ      └──────────┘└──────────────┘└┘└─┘
doc      └──────────┘                      
txt      └──────────┘                      
par      └──────────┘                      
pid           └────┘                      
st   ─────────────────────────────────────────┘└┘
274    induction e₂ with n₂ a₂ x₂ n₂ b₂ A₂ B₂ generalizing n₁ b₁,
id               └┘
src    └────────┘  └───────────────────────────────────────────┘
typ    └────────┘└┘└───────────────────────────────────────────┘
doc    └────────┘  └───────────────────────────────────────────┘
txt    └────────┘  └───────────────────────────────────────────┘
par    └────────┘  └───────────────────────────────────────────┘
pid               └───────────────────────┘└─────────────────┘
st   ──────────────────────────────────────────────────────────┘└─
275    { rcases cs₂ with ⟨n₂, rfl⟩,
id              └─┘
src      └─────┘   └─────────────┘
typ      └─────┘└─┘└─────────────┘
doc      └─────┘   └─────────────┘
txt      └─────┘   └─────────────┘
par      └─────┘   └─────────────┘
pid               └─────────────┘
st   ───┘└───────────────────────┘└─
276      simp! [cseval_add_const t n₂ cs₁] },
id              └──────────────┘  └┘ └─┘
src      └─────┘└──────────────┘      └┘
typ      └─────┘└──────────────┘└┘└─┘└┘
doc      └─────┘                      └┘
txt      └─────┘                      └┘
par      └─────┘                      └┘
pid                                
st   ─────────────────────────────────────┘└┘
277    cases cs₁ with csa₁ csb₁, cases id cs₂ with csa₂ csb₂,
id           └─┘                       └┘ └─┘
src    └────┘   └─────────────┘  └────┘└┘   └─────────────┘
typ    └────┘└─┘└─────────────┘  └────┘└┘└─┘└─────────────┘
doc    └────┘   └─────────────┘  └────┘     └─────────────┘
txt    └────┘   └─────────────┘  └────┘     └─────────────┘
par    └────┘   └─────────────┘  └────┘     └─────────────┘
pid            └─────────────┘            └─────────────┘
st   ─────────────────────────┘└───────────────────────────┘└─
278    simp!, have C := pos_num.cmp_to_nat x₁ x₂,
id                      └────────────────┘ └┘ └┘
src    └───┘  └────────┘└────────────────┘  
typ    └───┘  └────────┘└────────────────┘└┘└┘
doc    └───┘  └────────┘                    
txt    └───┘  └────────┘                    
par    └───┘  └────────┘                    
pid          └────┘└─┘                    
st   ──────┘└──────────────────────────────────┘└─
279    cases pos_num.cmp x₁ x₂; simp!,
id           └─────────┘ └┘ └┘
src    └────┘└─────────┘      └───┘
typ    └────┘└─────────┘└┘└┘  └───┘
doc    └────┘                 └───┘
txt    └────┘                 └───┘
par    └────┘                 └───┘
pid                              
st   ───────────────────────────────┘└─
280    { rcases B₁ csb₁ cs₂ with ⟨csh, h⟩,
id              └┘ └──┘ └─┘
src      └─────┘         └────────────┘
typ      └─────┘└┘└──┘└─┘└────────────┘
doc      └─────┘         └────────────┘
txt      └─────┘         └────────────┘
par      └─────┘         └────────────┘
pid                     └────────────┘
st   ───┘└──────────────────────────────┘└─
281      refine ⟨⟨csa₁, csh⟩, eq.symm _⟩,
id                └──┘  └─┘   └─────┘
src      └─────┘      └┘   └─┘└─────┘└─┘
typ      └─────┘  └──┘└┘└─┘└─┘└─────┘└─┘
doc      └─────┘      └┘   └─┘       └─┘
txt      └─────┘      └┘   └─┘       └─┘
par      └─────┘      └┘   └─┘       └─┘
pid                  └┘   └─┘       └─┘
st   ──────────────────────────────────┘└─
282      apply tactic.ring.horner_add_const,
id             └──────────────────────────┘
src      └────┘└──────────────────────────┘
typ      └────┘└──────────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────────────┘└─
283      exact h.symm },
id             └────┘
src      └────┘└────┘
typ      └────┘└────┘
doc      └────┘      
txt      └────┘      
par      └────┘      
pid                 
st   ────────────────┘└┘
284    { cases C,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────┘└─
285      have B0 : is_cs 0 → ∀ {e₂ : horner_expr}, is_cs e₂ →
id                 └───┘             └─────────┘
src      └────────┘     └─┘  └─────┘└─────────┘         
typ      └────────┘└───┘└─┘  └─────┘└─────────┘         
doc      └────────┘     └─┘  └─────┘└─────────┘         
txt      └────────┘     └─┘  └─────┘                    
par      └────────┘     └─┘  └─────┘                    
pid      └─────┘└─┘     └─┘  └─────┘                    
st   ─────────────────────────────────────────────────────────
286        is_cs (add 0 e₂) ∧ cseval t (add 0 e₂) = cseval t 0 + cseval t e₂ :=
id         └───┘                        └─┘                    └────┘ 
src  ─────┘└───┘    └─┘  └┘         └─┘└─┘  └┘       └─┘└────┘   └───
typ  ─────┘└───┘    └─┘  └┘         └─┘└─┘  └┘       └─┘└────┘  └───
doc  ─────┘└───┘    └─┘  └┘            └─┘  └┘        └─┘ └────┘   └───
txt  ─────┘         └─┘  └┘            └─┘  └┘        └─┘          └───
par  ─────┘         └─┘  └┘            └─┘  └┘        └─┘          └───
pid  ─────┘         └─┘  └┘            └─┘  └┘        └─┘          └───
st   ───────────────────────────────────────────────────────────────────────────
287        λ _ e₂ c, ⟨c, (zero_add _).symm⟩,
id                        └──────┘
src  ─────┘ └───────┘  └┘ └──────┘└───────┘
typ  ─────┘ └───────┘  └┘ └──────┘└───────┘
doc  ─────┘ └───────┘  └┘         └───────┘
txt  ─────┘ └───────┘  └┘         └───────┘
par  ─────┘ └───────┘  └┘         └───────┘
pid  ─────┘ └───────┘  └┘         └───────┘
st   ─────────────────────────────────────┘└─
288       cases e : num.sub' n₁ n₂ with k k; simp!,
id                  └──────┘ └┘ └┘
src       └────┘ └─┘└──────┘    └───────┘  └───┘
typ       └────┘ └─┘└──────┘└┘└┘└───────┘  └───┘
doc       └────┘ └─┘            └───────┘  └───┘
txt       └────┘ └─┘            └───────┘  └───┘
par       └────┘ └─┘            └───────┘  └───┘
pid             └─┘            └───────┘      
st   ────────────────────────────────────────────┘└─
289      { have : n₁ = n₂,
id                └┘   └┘
src        └─────┘   
typ        └─────┘└┘ └┘
doc        └─────┘   
txt        └─────┘   
par        └─────┘   
pid        └───┘└┘   
st   ─────┘└────────────┘└─
290        { have := congr_arg (coe : znum → ℤ) e,
id                   └───────┘  └─┘   └──┘      
src          └──────┘└───────┘ └─┘└─┘└──┘  └┘
typ          └──────┘└───────┘ └─┘└─┘└──┘  └┘
doc          └──────┘             └─┘└──┘  └┘
txt          └──────┘             └─┘      └┘
par          └──────┘             └─┘      └┘
pid          └───┘└─┘             └─┘      └┘
st   ───────┘└──────────────────────────────────┘└─
291          simp at this,
src          └──────────┘
typ          └──────────┘
doc          └──────────┘
txt          └──────────┘
par          └──────────┘
pid              └─────┘
st   ───────────────────┘└─
292          have := sub_eq_zero.1 this,
id                   └─────────┘   └──┘
src          └──────┘└─────────┘└─┘
typ          └──────┘└─────────┘└─┘└──┘
doc          └──────┘           └─┘
txt          └──────┘           └─┘
par          └──────┘           └─┘
pid          └───┘└─┘           └─┘
st   ─────────────────────────────────┘└─
293          rw [← num.to_nat_to_int, ← num.to_nat_to_int] at this,
id                 └───────────────┘    └───────────────┘
src          └────┘└───────────────┘└──┘└───────────────┘└───────┘
typ          └────┘└───────────────┘└──┘└───────────────┘└───────┘
doc          └────┘                 └──┘                 └───────┘
txt          └────┘                 └──┘                 └───────┘
par          └────┘                 └──┘                 └───────┘
pid            └──┘                 └──┘                 └──────┘
st   ──────────────────────────────┘└───────────────────┘└──────┘└─
294          exact num.to_nat_inj.1 (int.coe_nat_inj this) },
id                 └────────────┘    └─────────────┘ └──┘
src          └────┘└────────────┘└─┘ └─────────────┘    └┘
typ          └────┘└────────────┘└─┘ └─────────────┘└──┘└┘
doc          └────┘              └─┘                    └┘
txt          └────┘              └─┘                    └┘
par          └────┘              └─┘                    └┘
pid                             └─┘                    
st   ─────────────────────────────────────────────────────┘└┘
295        subst n₂,
id               └┘
src        └────┘
typ        └────┘└┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────┘└─
296        rcases cseval_horner' _ _ _ _ _ _ _ with ⟨csh, h⟩,
id                └────────────┘
src        └─────┘└────────────┘└──────────────────────────┘
typ        └─────┘└────────────┘└──────────────────────────┘
doc        └─────┘              └──────────────────────────┘
txt        └─────┘              └──────────────────────────┘
par        └─────┘              └──────────────────────────┘
pid                            └──────────────────────────┘
st   ──────────────────────────────────────────────────────┘└─
297        { refine ⟨csh, h.trans (eq.symm _)⟩,
id                   └─┘  └─────┘  └─────┘
src          └─────┘    └┘└─────┘ └─────┘└──┘
typ          └─────┘ └─┘└┘└─────┘ └─────┘└──┘
doc          └─────┘    └┘               └──┘
txt          └─────┘    └┘               └──┘
par          └─────┘    └┘               └──┘
pid                    └┘               └──┘
st   ───────┘└───────────────────────────────┘└─
298          simp *,
src          └────┘
typ          └────┘
doc          └────┘
txt          └────┘
par          └────┘
pid              
st   ─────────────┘└─
299          apply tactic.ring.horner_add_horner_eq; try {refl},
id                 └──────────────────────────────┘
src          └────┘└──────────────────────────────┘  └───┘└──┘
typ          └────┘└──────────────────────────────┘  └───┘└──┘
doc          └────┘                                  └───┘└──┘
txt          └────┘                                  └───┘└──┘
par          └────┘                                  └───┘└──┘
pid                                                    └─────┘
st   ────────────────────────────────────────────────────┘└──┘└┘
300          simp },
src          └───┘
typ          └───┘
doc          └───┘
txt          └───┘
par          └───┘
pid              
st   ────────────┘└┘
301        all_goals {simp! *} },
src        └─────────┘└─────┘└┘
typ        └─────────┘└─────┘└┘
doc        └─────────┘└─────┘└┘
txt        └─────────┘└─────┘└┘
par        └─────────┘└─────┘└┘
pid                 └────────┘
st   ────────────────┘└─────┘└┘
302      { simp [B₁ csb₁ csb₂],
id               └┘ └──┘ └──┘
src        └────┘          
typ        └────┘└┘└──┘└──┘
doc        └────┘          
txt        └────┘          
par        └────┘          
pid                      
st   ─────┘└─────────────────┘└─
303        rcases A₂ csa₂ _ _ B0 ⟨csa₁, 0, rfl⟩ with ⟨csh, h⟩,
id                └┘ └──┘     └┘  └──┘     └─┘
src        └─────┘      └───┘       └───┘└─┘└─────────────┘
typ        └─────┘└┘└──┘└───┘└┘ └──┘└───┘└─┘└─────────────┘
doc        └─────┘      └───┘       └───┘   └─────────────┘
txt        └─────┘      └───┘       └───┘   └─────────────┘
par        └─────┘      └───┘       └───┘   └─────────────┘
pid                    └───┘       └───┘   └─────────────┘
st   ───────────────────────────────────────────────────────┘└─
304        refine ⟨csh, eq.symm _⟩,
id                 └─┘  └─────┘
src        └─────┘    └┘└─────┘└─┘
typ        └─────┘ └─┘└┘└─────┘└─┘
doc        └─────┘    └┘       └─┘
txt        └─────┘    └┘       └─┘
par        └─────┘    └┘       └─┘
pid                  └┘       └─┘
st   ────────────────────────────┘└─
305        rw [show id = add 0, from rfl, h],
id                  └┘  └─┘         └─┘  
src        └──┘    └┘ └─┘└───────┘└─┘└┘ 
typ        └──┘    └┘└─┘└───────┘└─┘└┘
doc        └──┘          └───────┘   └┘ 
txt        └──┘          └───────┘   └┘ 
par        └──┘          └───────┘   └┘ 
pid          └┘          └───────┘   └┘ 
st   ──────────────────────────────────┘└─┘└──
306        apply tactic.ring.horner_add_horner_gt,
id               └──────────────────────────────┘
src        └────┘└──────────────────────────────┘
typ        └────┘└──────────────────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ───────────────────────────────────────────┘└─
307        { change (_ + k : ℕ) = _,
id                      
src          └─────┘ └┘ └─┘ └┘ └┘
typ          └─────┘ └┘└─┘ └┘ └┘
doc          └─────┘ └┘  └─┘ └┘ └┘
txt          └─────┘ └┘  └─┘ └┘ └┘
par          └─────┘ └┘  └─┘ └┘ └┘
pid                 └┘  └─┘ └┘ └┘
st   ───────┘└────────────────────┘└─
308          rw [← int.coe_nat_inj', int.coe_nat_add,
id                 └──────────────┘  └─────────────┘
src          └────┘└──────────────┘└┘└─────────────┘└─
typ          └────┘└──────────────┘└┘└─────────────┘└─
doc          └────┘                └┘               └─
txt          └────┘                └┘               └─
par          └────┘                └┘               └─
pid            └──┘                └┘               └─
st   ─────────────────────────────┘└───────────────┘└─
309            eq_comm, ← sub_eq_iff_eq_add'],
id             └─────┘    └────────────────┘
src  ─────────┘└─────┘└──┘└────────────────┘
typ  ─────────┘└─────┘└──┘└────────────────┘
doc  ─────────┘       └──┘                  
txt  ─────────┘       └──┘                  
par  ─────────┘       └──┘                  
pid  ─────────┘       └──┘                  
st   ────────────────┘└────────────────────┘└──
310          simpa using congr_arg (coe : znum → ℤ) e },
id                       └───────┘  └─┘   └──┘      
src          └──────────┘└───────┘ └─┘└─┘└──┘  └┘ 
typ          └──────────┘└───────┘ └─┘└─┘└──┘  └┘
doc          └──────────┘             └─┘└──┘  └┘ 
txt          └──────────┘             └─┘      └┘ 
par          └──────────┘             └─┘      └┘ 
pid               └────┘             └─┘      └┘ 
st   ────────────────────────────────────────────────┘└┘
311        all_goals { apply add_comm } },
id                           └──────┘
src        └──────────┘└────┘└──────┘└┘
typ        └──────────┘└────┘└──────┘└┘
doc        └──────────┘└────┘        └┘
txt        └──────────┘└────┘        └┘
par        └──────────┘└────┘        └┘
pid                 └───────┘        └┘
st   ────────────────┘└──────────────┘└┘
312      { have : (horner a₂ x₁ (num.pos k) 0).is_cs := ⟨csa₂, 0, rfl⟩,
id                 └────┘ └┘ └┘  └─────┘                └──┘     └─┘
src        └─────┘ └────┘     └─────┘ └────────────┘     └───┘└─┘
typ        └─────┘ └────┘└┘└┘ └─────┘└────────────┘ └──┘└───┘└─┘
doc        └─────┘                    └────────────┘     └───┘   
txt        └─────┘                    └────────────┘     └───┘   
par        └─────┘                    └────────────┘     └───┘   
pid        └───┘└┘                    └───────┘└───┘     └───┘   
st   ────────────────────────────────────────────────────────────────┘└─
313        simp [B₁ csb₁ csb₂, A₁ csa₁ this],
id               └┘ └──┘ └──┘  └┘ └──┘ └──┘
src        └────┘          └┘          
typ        └────┘└┘└──┘└──┘└┘└┘└──┘└──┘
doc        └────┘          └┘          
txt        └────┘          └┘          
par        └────┘          └┘          
pid                      └┘          
st   ──────────────────────────────────────┘└─
314        symmetry, apply tactic.ring.horner_add_horner_lt,
id                         └──────────────────────────────┘
src        └──────┘  └────┘└──────────────────────────────┘
typ        └──────┘  └────┘└──────────────────────────────┘
doc        └──────┘  └────┘
txt        └──────┘  └────┘
par        └──────┘  └────┘
pid                       
st   ─────────────┘└──────────────────────────────────────┘└─
315        { change (_ + k : ℕ) = _,
id                       
src          └─────┘ └┘  └─┘ └┘ └┘
typ          └─────┘ └┘ └─┘ └┘ └┘
doc          └─────┘ └┘  └─┘ └┘ └┘
txt          └─────┘ └┘  └─┘ └┘ └┘
par          └─────┘ └┘  └─┘ └┘ └┘
pid                 └┘  └─┘ └┘ └┘
st   ───────┘└────────────────────┘└─
316            rw [← int.coe_nat_inj', int.coe_nat_add,
id                   └──────────────┘  └─────────────┘
src            └────┘└──────────────┘└┘└─────────────┘└─
typ            └────┘└──────────────┘└┘└─────────────┘└─
doc            └────┘                └┘               └─
txt            └────┘                └┘               └─
par            └────┘                └┘               └─
pid              └──┘                └┘               └─
st   ───────────────────────────────┘└───────────────┘└─
317              eq_comm, ← sub_eq_iff_eq_add', ← neg_inj', neg_sub],
id               └─────┘    └────────────────┘    └──────┘  └─────┘
src  ───────────┘└─────┘└──┘└────────────────┘└──┘└──────┘└┘└─────┘
typ  ───────────┘└─────┘└──┘└────────────────┘└──┘└──────┘└┘└─────┘
doc  ───────────┘       └──┘                  └──┘        └┘       
txt  ───────────┘       └──┘                  └──┘        └┘       
par  ───────────┘       └──┘                  └──┘        └┘       
pid  ───────────┘       └──┘                  └──┘        └┘       
st   ──────────────────┘└────────────────────┘└──────────┘└───────┘└──
318          simpa using congr_arg (coe : znum → ℤ) e },
id                       └───────┘  └─┘   └──┘      
src          └──────────┘└───────┘ └─┘└─┘└──┘  └┘ 
typ          └──────────┘└───────┘ └─┘└─┘└──┘  └┘
doc          └──────────┘             └─┘└──┘  └┘ 
txt          └──────────┘             └─┘      └┘ 
par          └──────────┘             └─┘      └┘ 
pid               └────┘             └─┘      └┘ 
st   ────────────────────────────────────────────────┘└┘
319        { refl }, { apply add_comm } } },
id                           └──────┘
src          └───┘     └────┘└──────┘
typ          └───┘     └────┘└──────┘
doc          └───┘     └────┘        
txt          └───┘     └────┘        
par          └───┘     └────┘        
pid                                
st   ───────┘└───┘└┘└────────────────┘└────┘
320    { rcases B₂ csb₂ _ _ B₁ ⟨csa₁, csb₁⟩ with ⟨csh, h⟩,
id              └┘ └──┘     └┘  └──┘  └──┘
src      └─────┘      └───┘       └┘    └─────────────┘
typ      └─────┘└┘└──┘└───┘└┘ └──┘└┘└──┘└─────────────┘
doc      └─────┘      └───┘       └┘    └─────────────┘
txt      └─────┘      └───┘       └┘    └─────────────┘
par      └─────┘      └───┘       └┘    └─────────────┘
pid                  └───┘       └┘    └─────────────┘
st   ───────────────────────────────────────────────────┘└─
321      refine ⟨⟨csa₂, csh⟩, eq.symm _⟩,
id                └──┘  └─┘   └─────┘
src      └─────┘      └┘   └─┘└─────┘└─┘
typ      └─────┘  └──┘└┘└─┘└─┘└─────┘└─┘
doc      └─────┘      └┘   └─┘       └─┘
txt      └─────┘      └┘   └─┘       └─┘
par      └─────┘      └┘   └─┘       └─┘
pid                  └┘   └─┘       └─┘
st   ──────────────────────────────────┘└─
322      apply tactic.ring.const_add_horner,
id             └──────────────────────────┘
src      └────┘└──────────────────────────┘
typ      └────┘└──────────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────────────┘└─
323      simp [h] }
id             
src      └────┘ └┘
typ      └────┘└┘
doc      └────┘ └┘
txt      └────┘ └┘
par      └────┘ └┘
pid           
st   ────────────┘└─
324  end
st   ──┘
325  
326  theorem cseval_mul_const {α} [comm_semiring α] (t : tree α)
id                                 └───────────┘        └──┘ 
src                                └───────────┘         └──┘
typ                                └───────────┘        └──┘ 
327    (k : num) {e : horner_expr} (cs : e.is_cs) :
id          └─┘       └─────────┘        └────┘
src         └─┘       └─────────┘         └────┘
typ         └─┘       └─────────┘        └────┘
doc         └─┘       └─────────┘         └────┘
328    (mul_const k.to_znum e).is_cs ∧
id      └───────┘ └──────┘  └───┘  
src     └───────┘  └──────┘   └───┘  
typ     └───────┘ └──────┘  └───┘  
doc                           └───┘
329      cseval t (mul_const k.to_znum e) = cseval t e * k :=
id       └────┘   └───────┘ └──────┘    └────┘    
src      └────┘    └───────┘  └──────┘     └────┘     
typ      └────┘   └───────┘ └──────┘    └────┘    
doc      └────┘                             └────┘
330  begin
st   └─────
331    simp [mul_const],
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                 
st   ─────────────────┘└─
332    split_ifs with h h,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid             └──────┘
st   ───────────────────┘└─
333    { cases (num.to_znum_inj.1 h : k = 0),
id              └─────────────┘       
src      └────┘ └─────────────┘└─┘ └─┘ └─┘
typ      └────┘ └─────────────┘└─┘└─┘└─┘
doc      └────┘                └─┘ └─┘  └─┘
txt      └────┘                └─┘ └─┘  └─┘
par      └────┘                └─┘ └─┘  └─┘
pid                           └─┘ └─┘  └─┘
st   ───┘└─────────────────────────────────┘└─
334      exact ⟨⟨0, rfl⟩, (mul_zero _).symm⟩ },
id                  └─┘    └──────┘
src      └────┘  └─┘└─┘└─┘ └──────┘└────────┘
typ      └────┘  └─┘└─┘└─┘ └──────┘└────────┘
doc      └────┘  └─┘   └─┘         └────────┘
txt      └────┘  └─┘   └─┘         └────────┘
par      └────┘  └─┘   └─┘         └────────┘
pid             └─┘   └─┘         └───────┘
st   ───────────────────────────────────────┘└┘
335    { cases (num.to_znum_inj.1 h : k = 1),
id              └─────────────┘      
src      └────┘ └─────────────┘└─┘ └─┘  └─┘
typ      └────┘ └─────────────┘└─┘└─┘ └─┘
doc      └────┘                └─┘ └─┘  └─┘
txt      └────┘                └─┘ └─┘  └─┘
par      └────┘                └─┘ └─┘  └─┘
pid                           └─┘ └─┘  └─┘
st   ───┘└─────────────────────────────────┘└─
336      exact ⟨cs, (mul_one _).symm⟩ },
id              └┘   └─────┘
src      └────┘   └┘ └─────┘└────────┘
typ      └────┘ └┘└┘ └─────┘└────────┘
doc      └────┘   └┘        └────────┘
txt      └────┘   └┘        └────────┘
par      └────┘   └┘        └────────┘
pid              └┘        └───────┘
st   ────────────────────────────────┘└┘
337    induction e with n a x n b A B; simp *,
id               
src    └────────┘ └─────────────────┘  └────┘
typ    └────────┘└─────────────────┘  └────┘
doc    └────────┘ └─────────────────┘  └────┘
txt    └────────┘ └─────────────────┘  └────┘
par    └────────┘ └─────────────────┘  └────┘
pid              └────────────────┘      
st   ───────────────────────────────────────┘└─
338    { rcases cs with ⟨n, rfl⟩,
id              └┘
src      └─────┘  └────────────┘
typ      └─────┘└┘└────────────┘
doc      └─────┘  └────────────┘
txt      └─────┘  └────────────┘
par      └─────┘  └────────────┘
pid              └────────────┘
st   ───┘└─────────────────────┘└─
339      suffices, refine ⟨⟨n * k, this⟩, _⟩,
id                              └──┘
src      └──────┘  └─────┘    └┘    └───┘
typ      └──────┘  └─────┘  └┘└──┘└───┘
doc      └──────┘  └─────┘     └┘    └───┘
txt      └──────┘  └─────┘     └┘    └───┘
par      └──────┘  └─────┘     └┘    └───┘
pid      └──────┘             └┘    └───┘
st   ───────────┘└─────────────────────────┘└─
340      swap, {cases n; cases k; refl},
id                            
src      └──┘   └────┘   └────┘   └──┘
typ      └──┘   └────┘  └────┘  └──┘
doc      └──┘   └────┘   └────┘   └──┘
txt      └──┘   └────┘   └────┘   └──┘
par      └──┘   └────┘   └────┘   └──┘
pid                          
st   ───────┘└───────────────────────┘└┘
341      rw [show _, from this], simp! },
id                        └──┘
src      └──┘    └───────┘      └────┘
typ      └──┘    └───────┘└──┘  └────┘
doc      └──┘    └───────┘      └────┘
txt      └──┘    └───────┘      └────┘
par      └──┘    └───────┘      └────┘
pid        └┘    └───────┘          
st   ────────────────────────┘└───────┘└┘
342    { cases cs, simp! *,
id             └┘
src      └────┘    └─────┘
typ      └────┘└┘  └─────┘
doc      └────┘    └─────┘
txt      └────┘    └─────┘
par      └────┘    └─────┘
pid                   
st   ───────────┘└───────┘└─
343      symmetry, apply tactic.ring.horner_mul_const; refl }
id                       └──────────────────────────┘
src      └──────┘  └────┘└──────────────────────────┘  └───┘
typ      └──────┘  └────┘└──────────────────────────┘  └───┘
doc      └──────┘  └────┘                              └───┘
txt      └──────┘  └────┘                              └───┘
par      └──────┘  └────┘                              └───┘
pid                                                       
st   ───────────┘└─────────────────────────────────────────┘└─
344  end
st   ──┘
345  
346  theorem cseval_mul {α} [comm_semiring α] (t : tree α)
id                           └───────────┘        └──┘ 
src                          └───────────┘         └──┘
typ                          └───────────┘        └──┘ 
347    {e₁ e₂ : horner_expr} (cs₁ : e₁.is_cs) (cs₂ : e₂.is_cs) :
id              └─────────┘         └┘└────┘         └┘└────┘
src             └─────────┘           └────┘           └────┘
typ             └─────────┘         └┘└────┘         └┘└────┘
doc             └─────────┘           └────┘           └────┘
348    (mul e₁ e₂).is_cs ∧
id      └─┘ └┘ └┘ └───┘  
src     └─┘       └───┘  
typ     └─┘ └┘ └┘ └───┘  
doc               └───┘
349    cseval t (mul e₁ e₂) = cseval t e₁ * cseval t e₂ :=
id     └────┘   └─┘ └┘ └┘   └────┘  └┘  └────┘  └┘
src    └────┘    └─┘         └────┘       └────┘
typ    └────┘   └─┘ └┘ └┘   └────┘  └┘  └────┘  └┘
doc    └────┘                 └────┘        └────┘
350  begin
st   └─────
351    induction e₁ with n₁ a₁ x₁ n₁ b₁ A₁ B₁ generalizing e₂; simp!,
id               └┘
src    └────────┘  └────────────────────────────────────────┘  └───┘
typ    └────────┘└┘└────────────────────────────────────────┘  └───┘
doc    └────────┘  └────────────────────────────────────────┘  └───┘
txt    └────────┘  └────────────────────────────────────────┘  └───┘
par    └────────┘  └────────────────────────────────────────┘  └───┘
pid               └───────────────────────┘└──────────────┘      
st   ──────────────────────────────────────────────────────────────┘└─
352    { rcases cs₁ with ⟨n₁, rfl⟩,
id              └─┘
src      └─────┘   └─────────────┘
typ      └─────┘└─┘└─────────────┘
doc      └─────┘   └─────────────┘
txt      └─────┘   └─────────────┘
par      └─────┘   └─────────────┘
pid               └─────────────┘
st   ───┘└───────────────────────┘└─
353      simpa [mul_comm] using cseval_mul_const t n₁ cs₂ },
id              └──────┘        └──────────────┘  └┘ └─┘
src      └─────┘└──────┘└──────┘└──────────────┘      
typ      └─────┘└──────┘└──────┘└──────────────┘└┘└─┘
doc      └─────┘        └──────┘                      
txt      └─────┘        └──────┘                      
par      └─────┘        └──────┘                      
pid                   └────┘                      
st   ────────────────────────────────────────────────────┘└┘
354    induction e₂ with n₂ a₂ x₂ n₂ b₂ A₂ B₂,
id               └┘
src    └────────┘  └────────────────────────┘
typ    └────────┘└┘└────────────────────────┘
doc    └────────┘  └────────────────────────┘
txt    └────────┘  └────────────────────────┘
par    └────────┘  └────────────────────────┘
pid               └───────────────────────┘
st   ───────────────────────────────────────┘└─
355    { rcases cs₂ with ⟨n₂, rfl⟩,
id              └─┘
src      └─────┘   └─────────────┘
typ      └─────┘└─┘└─────────────┘
doc      └─────┘   └─────────────┘
txt      └─────┘   └─────────────┘
par      └─────┘   └─────────────┘
pid               └─────────────┘
st   ───┘└───────────────────────┘└─
356      simpa! using cseval_mul_const t n₂ cs₁ },
id                    └──────────────┘  └┘ └─┘
src      └───────────┘└──────────────┘      
typ      └───────────┘└──────────────┘└┘└─┘
doc      └───────────┘                      
txt      └───────────┘                      
par      └───────────┘                      
pid           └────┘                      
st   ──────────────────────────────────────────┘└┘
357    cases cs₁ with csa₁ csb₁, cases id cs₂ with csa₂ csb₂,
id           └─┘                       └┘ └─┘
src    └────┘   └─────────────┘  └────┘└┘   └─────────────┘
typ    └────┘└─┘└─────────────┘  └────┘└┘└─┘└─────────────┘
doc    └────┘   └─────────────┘  └────┘     └─────────────┘
txt    └────┘   └─────────────┘  └────┘     └─────────────┘
par    └────┘   └─────────────┘  └────┘     └─────────────┘
pid            └─────────────┘            └─────────────┘
st   ─────────────────────────┘└───────────────────────────┘└─
358    simp!, have C := pos_num.cmp_to_nat x₁ x₂,
id                      └────────────────┘ └┘ └┘
src    └───┘  └────────┘└────────────────┘  
typ    └───┘  └────────┘└────────────────┘└┘└┘
doc    └───┘  └────────┘                    
txt    └───┘  └────────┘                    
par    └───┘  └────────┘                    
pid          └────┘└─┘                    
st   ──────┘└──────────────────────────────────┘└─
359    cases A₂ csa₂ with csA₂ hA₂,
id           └┘ └──┘
src    └────┘      └────────────┘
typ    └────┘└┘└──┘└────────────┘
doc    └────┘      └────────────┘
txt    └────┘      └────────────┘
par    └────┘      └────────────┘
pid               └────────────┘
st   ────────────────────────────┘└─
360    cases pos_num.cmp x₁ x₂; simp!,
id           └─────────┘ └┘ └┘
src    └────┘└─────────┘      └───┘
typ    └────┘└─────────┘└┘└┘  └───┘
doc    └────┘                 └───┘
txt    └────┘                 └───┘
par    └────┘                 └───┘
pid                              
st   ───────────────────────────────┘└─
361    { simp [A₁ csa₁ cs₂, B₁ csb₁ cs₂],
id             └┘ └──┘ └─┘  └┘ └──┘ └─┘
src      └────┘         └┘         
typ      └────┘└┘└──┘└─┘└┘└┘└──┘└─┘
doc      └────┘         └┘         
txt      └────┘         └┘         
par      └────┘         └┘         
pid                   └┘         
st   ───┘└─────────────────────────────┘└─
362      symmetry, apply tactic.ring.horner_mul_const; refl },
id                       └──────────────────────────┘
src      └──────┘  └────┘└──────────────────────────┘  └───┘
typ      └──────┘  └────┘└──────────────────────────┘  └───┘
doc      └──────┘  └────┘                              └───┘
txt      └──────┘  └────┘                              └───┘
par      └──────┘  └────┘                              └───┘
pid                                                       
st   ───────────┘└─────────────────────────────────────────┘└┘
363    { cases cseval_horner' t _ x₁ n₂ 0 csA₂ ⟨0, rfl⟩ with csh₁ h₁,
id             └────────────┘    └┘ └┘   └──┘     └─┘
src      └────┘└────────────┘ └─┘    └─┘     └─┘└─┘└────────────┘
typ      └────┘└────────────┘└─┘└┘└┘└─┘└──┘ └─┘└─┘└────────────┘
doc      └────┘               └─┘    └─┘     └─┘   └────────────┘
txt      └────┘               └─┘    └─┘     └─┘   └────────────┘
par      └────┘               └─┘    └─┘     └─┘   └────────────┘
pid                          └─┘    └─┘     └─┘   └───────────┘
st   ───┘└─────────────────────────────────────────────────────────┘└─
364      cases C, split_ifs,
id             
src      └────┘   └───────┘
typ      └────┘  └───────┘
doc      └────┘   └───────┘
txt      └────┘   └───────┘
par      └────┘   └───────┘
pid           
st   ──────────┘└─────────┘└─
365      { subst b₂,
id               └┘
src        └────┘
typ        └────┘└┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└──────┘└─
366        refine ⟨csh₁, h₁.trans (eq.symm _)⟩,
id                 └──┘  └──────┘  └─────┘
src        └─────┘     └┘└──────┘ └─────┘└──┘
typ        └─────┘ └──┘└┘└──────┘ └─────┘└──┘
doc        └─────┘     └┘                └──┘
txt        └─────┘     └┘                └──┘
par        └─────┘     └┘                └──┘
pid                   └┘                └──┘
st   ────────────────────────────────────────┘└─
367        apply tactic.ring.horner_mul_horner_zero; try {refl},
id               └────────────────────────────────┘
src        └────┘└────────────────────────────────┘  └───┘└──┘
typ        └────┘└────────────────────────────────┘  └───┘└──┘
doc        └────┘                                    └───┘└──┘
txt        └────┘                                    └───┘└──┘
par        └────┘                                    └───┘└──┘
pid                                                    └─────┘
st   ────────────────────────────────────────────────────┘└──┘└┘
368        simp! [hA₂] },
id                └─┘
src        └─────┘   └┘
typ        └─────┘└─┘└┘
doc        └─────┘   └┘
txt        └─────┘   └┘
par        └─────┘   └┘
pid               
st   ─────────────────┘└┘
369      { cases A₁ csa₁ csb₂ with csA₁ hA₁,
id               └┘ └──┘ └──┘
src        └────┘          └────────────┘
typ        └────┘└┘└──┘└──┘└────────────┘
doc        └────┘          └────────────┘
txt        └────┘          └────────────┘
par        └────┘          └────────────┘
pid                       └────────────┘
st   ─────────────────────────────────────┘└─
370        cases cseval_add t csh₁ _ with csh₂ h₂,
id               └────────┘  └──┘
src        └────┘└────────┘     └─────────────┘
typ        └────┘└────────┘└──┘└─────────────┘
doc        └────┘               └─────────────┘
txt        └────┘               └─────────────┘
par        └────┘               └─────────────┘
pid                            └┘└───────────┘
st   ───────────────────────────────────────────┘└─
371        { refine ⟨csh₂, h₂.trans (eq.symm _)⟩,
id                   └──┘  └──────┘  └─────┘
src          └─────┘     └┘└──────┘ └─────┘└──┘
typ          └─────┘ └──┘└┘└──────┘ └─────┘└──┘
doc          └─────┘     └┘                └──┘
txt          └─────┘     └┘                └──┘
par          └─────┘     └┘                └──┘
pid                     └┘                └──┘
st   ───────┘└─────────────────────────────────┘└─
372          apply tactic.ring.horner_mul_horner; try {refl},
id                 └───────────────────────────┘
src          └────┘└───────────────────────────┘  └───┘└──┘
typ          └────┘└───────────────────────────┘  └───┘└──┘
doc          └────┘                               └───┘└──┘
txt          └────┘                               └───┘└──┘
par          └────┘                               └───┘└──┘
pid                                                 └─────┘
st   ─────────────────────────────────────────────────┘└──┘└┘
373          simp! * },
src          └──────┘
typ          └──────┘
doc          └──────┘
txt          └──────┘
par          └──────┘
pid              
st   ───────────────┘└┘
374        exact ⟨csA₁, (B₁ csb₁ csb₂).1⟩ } },
id                └──┘   └┘ └──┘ └──┘
src        └────┘     └┘           └───┘
typ        └────┘ └──┘└┘ └┘└──┘└──┘└───┘
doc        └────┘     └┘           └───┘
txt        └────┘     └┘           └───┘
par        └────┘     └┘           └───┘
pid                  └┘           └──┘
st   ────────────────────────────────────┘└──┘
375    { simp [A₂ csa₂, B₂ csb₂], rw [mul_comm, eq_comm],
id             └┘ └──┘  └┘ └──┘       └──────┘  └─────┘
src      └────┘      └┘        └──┘└──────┘└┘└─────┘
typ      └────┘└┘└──┘└┘└┘└──┘  └──┘└──────┘└┘└─────┘
doc      └────┘      └┘        └──┘        └┘       
txt      └────┘      └┘        └──┘        └┘       
par      └────┘      └┘        └──┘        └┘       
pid                └┘          └┘        └┘       
st   ──────────────────────────┘└────────────┘└───────┘└─
376      apply tactic.ring.horner_const_mul,
id             └──────────────────────────┘
src      └────┘└──────────────────────────┘
typ      └────┘└──────────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────────────┘└─
377      {apply mul_comm}, {refl} },
id              └──────┘
src       └────┘└──────┘    └──┘
typ       └────┘└──────┘    └──┘
doc       └────┘            └──┘
txt       └────┘            └──┘
par       └────┘            └──┘
pid            
st   ──────────────────┘└┘└────┘└────
378  end
st   ──┘
379  
380  theorem cseval_pow {α} [comm_semiring α] (t : tree α)
id                           └───────────┘        └──┘ 
src                          └───────────┘         └──┘
typ                          └───────────┘        └──┘ 
381    {x : horner_expr} (cs : x.is_cs) :
id          └─────────┘        └────┘
src         └─────────┘         └────┘
typ         └─────────┘        └────┘
doc         └─────────┘         └────┘
382    ∀ (n : num), (pow x n).is_cs ∧
id           └─┘    └─┘   └───┘  
src           └─┘    └─┘     └───┘  
typ          └─┘    └─┘   └───┘  
doc           └─┘            └───┘
383      cseval t (pow x n) = cseval t x ^ (n : ℕ)
id       └────┘   └─┘     └────┘        
src      └────┘    └─┘       └────┘           
typ      └────┘   └─┘     └────┘        
doc      └────┘               └────┘
384  | 0 := ⟨⟨1, rfl⟩, (pow_zero _).symm⟩
id               └─┘    └──────┘   └──┘
src              └─┘    └──────┘   └──┘
typ              └─┘    └──────┘   └──┘
385  | (num.pos p) := begin
id      └─────┘
src     └─────┘
typ     └─────┘
st                    └─────
386    simp [pow], induction p with p ep p ep,
id           └─┘             
src    └────┘└─┘  └────────┘ └─────────────┘
typ    └────┘└─┘  └────────┘└─────────────┘
doc    └────┘     └────────┘ └─────────────┘
txt    └────┘     └────────┘ └─────────────┘
par    └────┘     └────────┘ └─────────────┘
pid                       └────────────┘
st   ───────────┘└──────────────────────────┘└─
387    { simp * },
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid          
st   ───┘└─────┘└┘
388    { simp [pow_bit1],
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                  
st   ───┘└─────────────┘└─
389      cases cseval_mul t ep.1 ep.1 with cs₀ h₀,
id             └────────┘       └┘
src      └────┘└────────┘   └─┘  └────────────┘
typ      └────┘└────────┘  └─┘└┘└────────────┘
doc      └────┘             └─┘  └────────────┘
txt      └────┘             └─┘  └────────────┘
par      └────┘             └─┘  └────────────┘
pid                        └─┘  └────────────┘
st   ───────────────────────────────────────────┘└─
390      cases cseval_mul t cs₀ cs with cs₁ h₁,
id             └────────┘  └─┘ └┘
src      └────┘└────────┘      └──────────┘
typ      └────┘└────────┘└─┘└┘└──────────┘
doc      └────┘                └──────────┘
txt      └────┘                └──────────┘
par      └────┘                └──────────┘
pid                           └──────────┘
st   ────────────────────────────────────────┘└─
391      simp * },
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid          
st   ──────────┘└┘
392    { simp [pow_bit0],
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                  
st   ──────────────────┘└─
393      cases cseval_mul t ep.1 ep.1 with cs₀ h₀,
id             └────────┘       └┘
src      └────┘└────────┘   └─┘  └────────────┘
typ      └────┘└────────┘  └─┘└┘└────────────┘
doc      └────┘             └─┘  └────────────┘
txt      └────┘             └─┘  └────────────┘
par      └────┘             └─┘  └────────────┘
pid                        └─┘  └────────────┘
st   ───────────────────────────────────────────┘└─
394      simp * }
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid          
st   ──────────┘└─
395  end
st   ──┘
396  
397  /-- For any given tree `t` of atoms and any reflected expression `r`,
398  the Horner form of `r` is a valid csring expression, and under `t`,
399  the Horner form evaluates to the same thing as `r`. -/
400  theorem cseval_of_csexpr {α} [comm_semiring α] (t : tree α) :
id                                 └───────────┘        └──┘ 
src                                └───────────┘         └──┘
typ                                └───────────┘        └──┘ 
401    ∀ (r : csring_expr), (of_csexpr r).is_cs ∧ cseval t (of_csexpr r) = r.eval t
id           └─────────┘    └───────┘  └───┘   └────┘   └───────┘    └───┘ 
src           └─────────┘    └───────┘   └───┘   └────┘    └───────┘      └───┘
typ          └─────────┘    └───────┘  └───┘   └────┘   └───────┘    └───┘ 
doc           └─────────┘    └───────┘   └───┘    └────┘    └───────┘       └───┘
402  | (csring_expr.atom n)  := cseval_atom _ _
id      └──────────────┘        └─────────┘
src     └──────────────┘        └─────────┘
typ     └──────────────┘        └─────────┘
403  | (csring_expr.const n) := ⟨⟨n, rfl⟩, by cases n; refl⟩
id      └───────────────┘           └─┘            
src     └───────────────┘            └─┘      └────┘   └──┘
typ     └───────────────┘           └─┘      └────┘  └──┘
doc                                           └────┘   └──┘
txt                                           └────┘   └──┘
par                                           └────┘   └──┘
pid                                                
st                                           └────────────┘
404  | (csring_expr.add x y) :=
id      └─────────────┘  
src     └─────────────┘
typ     └─────────────┘  
405    let ⟨cs₁, h₁⟩ := cseval_of_csexpr x,
id     └─┘  └─┘         └──────────────┘
typ    └─┘  └─┘         └──────────────┘
406        ⟨cs₂, h₂⟩ := cseval_of_csexpr y,
id          └─┘         └──────────────┘
typ         └─┘         └──────────────┘
407        ⟨cs, h⟩ := cseval_add t cs₁ cs₂ in ⟨cs, by simp! [h, *]⟩
id          └┘        └────────┘                            
src                   └────────┘                      └─────┘ └──┘
typ         └┘        └────────┘                     └─────┘└──┘
doc                                                   └─────┘ └──┘
txt                                                   └─────┘ └──┘
par                                                   └─────┘ └──┘
pid                                                        └──┘
st                                                   └───────────┘
408  | (csring_expr.mul x y) :=
id      └─────────────┘  
src     └─────────────┘
typ     └─────────────┘  
409    let ⟨cs₁, h₁⟩ := cseval_of_csexpr x,
id     └─┘  └─┘         └──────────────┘
typ    └─┘  └─┘         └──────────────┘
410        ⟨cs₂, h₂⟩ := cseval_of_csexpr y,
id          └─┘         └──────────────┘
typ         └─┘         └──────────────┘
411        ⟨cs, h⟩ := cseval_mul t cs₁ cs₂ in ⟨cs, by simp! [h, *]⟩
id          └┘        └────────┘                            
src                   └────────┘                      └─────┘ └──┘
typ         └┘        └────────┘                     └─────┘└──┘
doc                                                   └─────┘ └──┘
txt                                                   └─────┘ └──┘
par                                                   └─────┘ └──┘
pid                                                        └──┘
st                                                   └───────────┘
412  | (csring_expr.pow x n) :=
id      └─────────────┘  
src     └─────────────┘
typ     └─────────────┘  
413    let ⟨cs, h⟩ := cseval_of_csexpr x,
id     └─┘  └┘        └──────────────┘
typ    └─┘  └┘        └──────────────┘
414        ⟨cs, h⟩ := cseval_pow t cs n in ⟨cs, by simp! [h, *]⟩
id          └┘        └────────┘                         
src                   └────────┘                   └─────┘ └──┘
typ         └┘        └────────┘                  └─────┘└──┘
doc                                                └─────┘ └──┘
txt                                                └─────┘ └──┘
par                                                └─────┘ └──┘
pid                                                     └──┘
st                                                └───────────┘
415  
416  end horner_expr
417  
418  /-- The main proof-by-reflection theorem. Given reflected csring expressions
419  `r₁` and `r₂` plus a storage `t` of atoms, if both expressions go to the
420  same Horner normal form, then the original non-reflected expressions are
421  equal. `H` follows from kernel reduction and is therefore `rfl`. -/
422  theorem correctness {α} [comm_semiring α] (t : tree α) (r₁ r₂ : csring_expr)
id                            └───────────┘        └──┘            └─────────┘
src                           └───────────┘         └──┘             └─────────┘
typ                           └───────────┘        └──┘            └─────────┘
doc                                                                  └─────────┘
423    (H : horner_expr.of_csexpr r₁ = horner_expr.of_csexpr r₂) :
id          └───────────────────┘ └┘  └───────────────────┘ └┘
src         └───────────────────┘     └───────────────────┘
typ         └───────────────────┘ └┘  └───────────────────┘ └┘
doc         └───────────────────┘      └───────────────────┘
424    r₁.eval t = r₂.eval t :=
id     └┘└───┘   └┘└───┘ 
src      └───┘      └───┘
typ    └┘└───┘   └┘└───┘ 
doc      └───┘       └───┘
425  by repeat {rw ← (horner_expr.cseval_of_csexpr t _).2}; rw H
id                    └──────────────────────────┘            
src     └──────┘└───┘ └──────────────────────────┘ └───┘  └─┘ 
typ     └──────┘└───┘ └──────────────────────────┘└───┘  └─┘
doc     └──────┘└───┘ └──────────────────────────┘ └───┘  └─┘ 
txt     └──────┘└───┘                              └───┘  └─┘ 
par     └──────┘└───┘                              └───┘  └─┘ 
pid           └─────┘                              └────┘     
st     └────────────────────────────────────────────────┘└┘└──┘
426  
src  
typ  
doc  
txt  
par  
pid  
st   
427  /-- Reflects a csring expression into a `csring_expr`, together
428  with a dlist of atoms, i.e. opaque variables over which the
429  expression is a polynomial. -/
430  meta def reflect_expr : expr → csring_expr × dlist expr
id                           └──┘  └─────────┘  └───┘ └──┘
src                          └──┘   └─────────┘  └───┘ └──┘
typ                          └──┘  └─────────┘  └───┘ └──┘
doc                          └──┘   └─────────┘   └───┘ └──┘
431  | `(%%e₁ + %%e₂) :=
id         └┘    └┘
src           
typ        └┘    └┘
432    let (r₁, l₁) := reflect_expr e₁, (r₂, l₂) := reflect_expr e₂ in
id     └─┘ └┘  └┘     └──────────┘     └┘  └┘     └──────────┘
src                                    
typ    └─┘ └┘  └┘     └──────────┘     └┘  └┘     └──────────┘
433    (r₁.add r₂, l₁ ++ l₂)
id       └──┘        └┘
src      └──┘        └┘
typ      └──┘        └┘
434  /-| `(%%e₁ - %%e₂) :=
435    let (r₁, l₁) := reflect_expr e₁, (r₂, l₂) := reflect_expr e₂ in
436    (r₁.add r₂.neg, l₁ ++ l₂)
437  | `(- %%e) := let (r, l) := reflect_expr e in (r.neg, l)-/
438  | `(%%e₁ * %%e₂) :=
id         └┘    └┘
src           
typ        └┘    └┘
439    let (r₁, l₁) := reflect_expr e₁, (r₂, l₂) := reflect_expr e₂ in
id     └─┘ └┘  └┘     └──────────┘     └┘  └┘     └──────────┘
src                                    
typ    └─┘ └┘  └┘     └──────────┘     └┘  └┘     └──────────┘
440    (r₁.mul r₂, l₁ ++ l₂)
id       └──┘        └┘
src      └──┘        └┘
typ      └──┘        └┘
441  /-| `(has_inv.inv %%e) := let (r, l) := reflect_expr e in (r.neg, l)
442  | `(%%e₁ / %%e₂) :=
443    let (r₁, l₁) := reflect_expr e₁, (r₂, l₂) := reflect_expr e₂ in
444    (r₁.mul r₂.inv, l₁ ++ l₂)-/
445  | e@`(%%e₁ ^ %%e₂) :=
id           └┘    └┘
src             
typ          └┘    └┘
446    match reflect_expr e₁, expr.to_nat e₂ with
id           └──────────┘     └─────────┘
src                           └─────────┘
typ          └──────────┘     └─────────┘
doc                           └─────────┘
447    | (r₁, l₁), some n₂ := (r₁.pow (num.of_nat' n₂), l₁)
id       └┘  └┘   └──┘ └┘      └──┘  └─────────┘
src               └──┘         └──┘  └─────────┘
typ      └┘  └┘   └──┘ └┘      └──┘  └─────────┘
448    | (r₁, l₁), none := (csring_expr.atom 1, dlist.singleton e)
id                └──┘    └──────────────┘    └─────────────┘
src               └──┘    └──────────────┘    └─────────────┘
typ               └──┘    └──────────────┘    └─────────────┘
doc                                             └─────────────┘
449    end
450  | e := match expr.to_nat e with
id               └─────────┘
src               └─────────┘
typ              └─────────┘
doc               └─────────┘
451    | some n := (csring_expr.const (num.of_nat' n), dlist.empty)
id       └──┘     └───────────────┘  └─────────┘     └─────────┘
src      └──┘      └───────────────┘  └─────────┘     └─────────┘
typ      └──┘     └───────────────┘  └─────────┘     └─────────┘
doc                                                    └─────────┘
452    | none := (csring_expr.atom 1, dlist.singleton e)
id       └──┘    └──────────────┘    └─────────────┘
src      └──┘    └──────────────┘    └─────────────┘
typ      └──┘    └──────────────┘    └─────────────┘
doc                                   └─────────────┘
453    end
454  
455  /-- In the output of `reflect_expr`, `atom`s are initialized with incorrect indices.
456  The indices cannot be computed until the whole tree is built, so another pass over
457  the expressions is needed - this is what `replace` does. The computation (expressed
458  in the state monad) fixes up `atom`s to match their positions in the atom tree.
459  The initial state is a list of all atom occurrences in the goal, left-to-right. -/
460  meta def csring_expr.replace (t : tree expr) : csring_expr → state_t (list expr) option csring_expr
id                                     └──┘ └──┘    └─────────┘  └─────┘  └──┘ └──┘  └────┘ └─────────┘
src                                    └──┘ └──┘    └─────────┘   └─────┘  └──┘ └──┘  └────┘ └─────────┘
typ                                    └──┘ └──┘    └─────────┘  └─────┘  └──┘ └──┘  └────┘ └─────────┘
doc                                         └──┘    └─────────┘                 └──┘         └─────────┘
461  | (csring_expr.atom _)  := do e ← get,
id      └──────────────┘              └─┘
src     └──────────────┘               └─┘
typ     └──────────────┘              └─┘
doc                                    └─┘
462    p ← monad_lift (t.index_of (<) e.head),
id        └────────┘  └───────┘    └───┘
src        └────────┘   └───────┘     └───┘
typ       └────────┘  └───────┘    └───┘
doc                     └───────┘
463    put e.tail, pure (csring_expr.atom p)
id     └─┘ └───┘  └──┘  └──────────────┘ 
src    └─┘  └───┘  └──┘  └──────────────┘
typ    └─┘ └───┘  └──┘  └──────────────┘ 
doc    └─┘
464  | (csring_expr.const n) := pure (csring_expr.const n)
id      └───────────────┘      └──┘  └───────────────┘
src     └───────────────┘       └──┘  └───────────────┘
typ     └───────────────┘      └──┘  └───────────────┘
465  | (csring_expr.add x y) := csring_expr.add <$> x.replace <*> y.replace
id      └─────────────┘       └─────────────┘ └─┘           └─┘
src     └─────────────┘         └─────────────┘ └─┘           └─┘
typ     └─────────────┘       └─────────────┘ └─┘           └─┘
466  | (csring_expr.mul x y) := csring_expr.mul <$> x.replace <*> y.replace
id      └─────────────┘       └─────────────┘ └─┘           └─┘
src     └─────────────┘         └─────────────┘ └─┘           └─┘
typ     └─────────────┘       └─────────────┘ └─┘           └─┘
467  | (csring_expr.pow x n) := (λ x, csring_expr.pow x n) <$> x.replace
id      └─────────────┘            └─────────────┘     └─┘
src     └─────────────┘               └─────────────┘      └─┘
typ     └─────────────┘            └─────────────┘     └─┘
468  --| (csring_expr.neg x)   := csring_expr.neg <$> x.replace
469  --| (csring_expr.inv x)   := csring_expr.inv <$> x.replace
470  
471  end tactic.ring2
472  
473  namespace tactic
474  namespace interactive
475  open interactive interactive.types lean.parser
476  open tactic.ring2
477  
478  local postfix `?`:9001 := optional
id                             └──────┘
src                            └──────┘
typ                            └──────┘
479  
480  /-- Tactic for solving equations in the language of rings.
481    This variant on the `ring` tactic uses kernel computation instead
482    of proof generation. -/
483  meta def ring2 : tactic unit :=
id                    └────┘ └──┘
src                   └────┘ └──┘
typ                   └────┘ └──┘
doc                          └──┘
484  do `[repeat {rw ← nat.pow_eq_pow}],
src       └──────┘└───┘              
typ       └──────┘└───┘              
doc       └──────┘└───┘              
txt       └──────┘└───┘              
par       └──────┘└───┘              
pid             └─────┘              
485    `(%%e₁ = %%e₂) ← target
id     └┘  └┘    └┘    └────┘
src    └┘              └────┘
typ    └┘  └┘    └┘    └────┘
doc    └┘               └────┘
486    | fail "ring2 tactic failed: the goal is not an equality",
id       └──┘
src      └──┘
typ      └──┘
487    α ← infer_type e₁,
id        └────────┘
src        └────────┘
typ       └────────┘
doc        └────────┘
488    expr.sort (level.succ u) ← infer_type α,
id     └───────┘  └────────┘     └────────┘ 
src    └───────┘  └────────┘      └────────┘
typ    └───────┘  └────────┘     └────────┘ 
doc                               └────────┘
489    let (r₁, l₁) := reflect_expr e₁,
id     └─┘ └┘  └┘     └──────────┘
src                   └──────────┘
typ    └─┘ └┘  └┘     └──────────┘
doc                    └──────────┘
490    let (r₂, l₂) := reflect_expr e₂,
id         └┘  └┘     └──────────┘
src                   └──────────┘
typ        └┘  └┘     └──────────┘
doc                    └──────────┘
491    let L := (l₁ ++ l₂).to_list,
id                 └┘    └─────┘
src                 └┘    └─────┘
typ                └┘    └─────┘
doc                       └─────┘
492    let s := tree.of_rbnode (rbtree_of L).1,
id             └────────────┘  └───────┘  
src             └────────────┘  └───────┘   
typ            └────────────┘  └───────┘  
doc             └────────────┘
493    (r₁, L) ← (state_t.run (r₁.replace s) L : option _),
id     └┘       └─────────┘    └──────┘      └────┘
src              └─────────┘    └──────┘        └────┘
typ    └┘       └─────────┘    └──────┘      └────┘
doc                              └──────┘
494    (r₂, _) ← (state_t.run (r₂.replace s) L : option _),
id     └┘        └─────────┘    └──────┘       └────┘
src              └─────────┘    └──────┘        └────┘
typ    └┘        └─────────┘    └──────┘       └────┘
doc                              └──────┘
495    let se : expr := s.reflect' u α,
id              └──┘    └───────┘   
src             └──┘     └───────┘
typ             └──┘    └───────┘   
doc             └──┘     └───────┘
496    let er₁ : expr := reflect r₁,
id               └──┘    └─────┘
src              └──┘    └─────┘
typ              └──┘    └─────┘
doc              └──┘
497    let er₂ : expr := reflect r₂,
id               └──┘    └─────┘
src              └──┘    └─────┘
typ              └──┘    └─────┘
doc              └──┘
498    cs ← mk_app ``comm_semiring [α] >>= mk_instance,
id     └┘   └────┘                 └─┘ └─────────┘
src         └────┘                  └─┘ └─────────┘
typ    └┘   └────┘                 └─┘ └─────────┘
doc         └────┘                         └─────────┘
499    e ← to_expr ``(correctness %%se %%er₁ %%er₂ rfl)
id        └─────┘    └─────────┘   └┘   └─┘   └─┘ └─┘
src        └─────┘    └─────────┘                  └─┘
typ       └─────┘    └─────────┘   └┘   └─┘   └─┘ └─┘
doc        └─────┘    └─────────┘
500      <|> fail ("ring2 tactic failed, cannot show equality:\n"
id       └─┘ └──┘
src      └─┘ └──┘
typ      └─┘ └──┘
501        ++ to_string (horner_expr.of_csexpr r₁) ++
id         └┘ └───────┘  └───────────────────┘     └┘
src        └┘ └───────┘  └───────────────────┘     └┘
typ        └┘ └───────┘  └───────────────────┘     └┘
doc                      └───────────────────┘
502        "\n  =?=\n" ++ to_string (horner_expr.of_csexpr r₂)),
id                     └┘ └───────┘  └───────────────────┘
src                    └┘ └───────┘  └───────────────────┘
typ                    └┘ └───────┘  └───────────────────┘
doc                                  └───────────────────┘
503    tactic.exact e
id     └──────────┘ 
src    └──────────┘
typ    └──────────┘ 
doc    └──────────┘
504  
505  end interactive
506  end tactic
507  
508  namespace conv.interactive
509  open conv
510  
511  meta def ring2 : conv unit := discharge_eq_lhs tactic.interactive.ring2
id                    └──┘ └──┘    └──────────────┘ └──────────────────────┘
src                   └──┘ └──┘    └──────────────┘ └──────────────────────┘
typ                   └──┘ └──┘    └──────────────┘ └──────────────────────┘
doc                        └──┘                     └──────────────────────┘
512  
513  end conv.interactive